﻿#include <iostream>
#include <fstream>
#include <vector>
#include <chrono>
#include <sstream>
#include <unordered_map>
#include <unordered_set>
#include <stack>
#include <queue>
#include <random>
#include <ctime>
using namespace std;
using namespace chrono;
struct Node {
    int var;
    bool negated;
    Node() : var(0), negated(false) {} 
    Node(int v, bool n) : var(v), negated(n) {}
};
struct CNFFormula {
    int numVars;
    vector<vector<Node>> clauses;
    vector<vector<int>*> positiveLiteralToClauses; 
    vector<vector<int>*> negativeLiteralToClauses;  
    vector<unordered_set<int>> clauseToLiterals;    // 子句到字面量的映射

    CNFFormula(int nVars) : numVars(nVars) {
        positiveLiteralToClauses.resize(numVars + 1);
        negativeLiteralToClauses.resize(numVars + 1);
    }

    void addClause(const vector<Node>& clause) {
        int clauseIndex = clauses.size();
        clauses.push_back(clause);
        unordered_set<int> literals;

        for (const auto& node : clause) {
            int literal = node.var * (node.negated ? 1 : -1);
            literals.insert(literal);
            if (literal > 0) {
                if (!positiveLiteralToClauses[literal]) {
                    positiveLiteralToClauses[literal] = new vector<int>();
                }
                positiveLiteralToClauses[literal]->push_back(clauseIndex);
            }
            else {
                int var = -literal;
                if (!negativeLiteralToClauses[var]) {
                    negativeLiteralToClauses[var] = new vector<int>();
                }
                negativeLiteralToClauses[var]->push_back(clauseIndex);
            }
        }
        clauseToLiterals.push_back(literals);
    }

    void removeClause(int clauseIndex) {
        if (clauseIndex >= clauseToLiterals.size()) return;
        for (int literal : clauseToLiterals[clauseIndex]) {
            if (literal > 0 && positiveLiteralToClauses[literal]) {
                auto& clauses = *positiveLiteralToClauses[literal];
                clauses.erase(remove(clauses.begin(), clauses.end(), clauseIndex), clauses.end());
            }
            else if (literal < 0 && negativeLiteralToClauses[-literal]) {
                auto& clauses = *negativeLiteralToClauses[-literal];
                clauses.erase(remove(clauses.begin(), clauses.end(), clauseIndex), clauses.end());
            }
        }
        clauseToLiterals[clauseIndex].clear();
    }

    const vector<int>& getClausesWithLiteral(int literal) const {
        if (literal > 0) {
            return *positiveLiteralToClauses[literal];
        }
        else {
            return *negativeLiteralToClauses[-literal];
        }
    }

};


milliseconds totalFindingTime(0);

CNFFormula readCNF(const string& filename) {
    ifstream file(filename);
    CNFFormula cnf(0);  
    string line;
    int numVars = 0;  

    while (getline(file, line)) {
        if (line.empty() || line[0] == 'c') continue;  
        else if (line[0] == 'p') {  
            istringstream iss(line);
            string dummy;
            int numClauses;
            iss >> dummy >> dummy >> numVars >> numClauses;  
            cnf = CNFFormula(numVars);  
        }
        else {
            istringstream ss(line);
            int var;
            vector<Node> clause;
            while (ss >> var && var != 0) {
                clause.push_back(Node(abs(var), var > 0));  
            }
            cnf.addClause(clause);  
        }
    }

    return cnf;
}

bool isSatisfied(const CNFFormula& cnf, const vector<int>& assignment) {
    for (const auto& clause : cnf.clauses) {
        bool clauseSatisfied = false;
        for (const auto& node : clause) {
            if (assignment[node.var - 1] != -1) {
                bool value = assignment[node.var - 1];
                if (!node.negated) value = !value;
                if (value) {
                    clauseSatisfied = true;
                    break;
                }
            }
        }
        if (!clauseSatisfied) {
            return false;
        }
    }
    return true;
}

void pureLiteralElimination(CNFFormula& cnf, vector<int>& assignment, vector<bool>& clauseDeleted, vector<int>& pureLiterals) {
    vector<int> literalCount(cnf.numVars + 1, 0);
    vector<bool> isPureLiteral(cnf.numVars + 1, true);
    for (const auto& clause : cnf.clauses) {
        for (const auto& node : clause) {
            int literal = node.var * (node.negated ? 1 : -1);
            literalCount[abs(literal)]++;
            int oppositeLiteral = -literal;
            const vector<int>& oppositeClauses = cnf.getClausesWithLiteral(oppositeLiteral);
            if (&oppositeClauses != nullptr) {
                isPureLiteral[abs(literal)] = false; 
            }
            else {
            }
        }
    }
    unordered_set<int> clausesToRemove;
    for (int var = 1; var <= cnf.numVars; ++var) {
        if (isPureLiteral[var] && assignment[var - 1] == -1) {
            if (cnf.positiveLiteralToClauses[var] && !cnf.positiveLiteralToClauses[var]->empty()) {
                assignment[var - 1] = 1;  
                pureLiterals.push_back(var); 
            }
            else if (cnf.negativeLiteralToClauses[var] && !cnf.negativeLiteralToClauses[var]->empty()) {
                assignment[var - 1] = 0;  
                pureLiterals.push_back(-var);  
            }
            if (assignment[var - 1] == 1 && cnf.positiveLiteralToClauses[var]) {
                for (int clauseIndex : *cnf.positiveLiteralToClauses[var]) {
                    clauseDeleted[clauseIndex] = true;
                    clausesToRemove.insert(clauseIndex);
                }
            }
            else if (assignment[var - 1] == 0 && cnf.negativeLiteralToClauses[var]) {
                for (int clauseIndex : *cnf.negativeLiteralToClauses[var]) {
                    clauseDeleted[clauseIndex] = true;
                    clausesToRemove.insert(clauseIndex);
                }
            }
        }
    }
    for (int clauseIndex : clausesToRemove) {
        cnf.removeClause(clauseIndex);  
    }
}



bool propagateLiteral(int literal, const CNFFormula& cnf, vector<int>& assignment,
    vector<int>& clauseChangeLog, vector<bool>& clauseDeleted,
    vector<int>& unassignedCount, vector<Node>& lastUnassignedNode) {
    int var = abs(literal);
    bool value = literal > 0;
    if (assignment[var - 1] != -1) return true;

    assignment[var - 1] = value ? 1 : 0;
    const auto& relatedClauses1 = cnf.getClausesWithLiteral(literal);
    for (int clauseIndex : relatedClauses1) {
        if (clauseDeleted[clauseIndex]) continue;
        clauseDeleted[clauseIndex] = true;
        clauseChangeLog.push_back(clauseIndex);  
    }

    try {
        const auto& relatedClauses2 = cnf.getClausesWithLiteral(-literal);
    }
    catch (...) {
        return true;
    }
    const auto& relatedClauses2 = cnf.getClausesWithLiteral(-literal);
    if(&relatedClauses2 == nullptr){
        return true;
    }
    for (int clauseIndex : relatedClauses2) {
        if (clauseDeleted[clauseIndex]) continue;
        unassignedCount[clauseIndex] = 0;
        for (const auto& node : cnf.clauses[clauseIndex]) {
            int assignedValue = assignment[node.var - 1];
            if (assignedValue == (node.negated ? 1 : 0)) {
                clauseDeleted[clauseIndex] = true;
                clauseChangeLog.push_back(clauseIndex);  
                break;
            }
            if (assignedValue == -1) {
                unassignedCount[clauseIndex]++;
                lastUnassignedNode[clauseIndex] = node;
            }
        }

        if (unassignedCount[clauseIndex] == 0 && !clauseDeleted[clauseIndex]) {
            return false; // 发现冲突，终止传播
        }

        if (unassignedCount[clauseIndex] == 1 && !clauseDeleted[clauseIndex]) {
            int newLiteral = lastUnassignedNode[clauseIndex].var * (lastUnassignedNode[clauseIndex].negated ? 1 : -1);
            if (!propagateLiteral(newLiteral, cnf, assignment, clauseChangeLog, clauseDeleted, unassignedCount, lastUnassignedNode)) {
                return false; 
            }
        }
    }
    return true;
}

bool unitPropagation(CNFFormula& cnf, vector<int>& assignment,
    vector<int>& clauseChangeLog, vector<bool>& clauseDeleted, 
    vector<int>& unassignedCount, vector<Node>& lastUnassignedNode) {
    for (int i = 0; i < cnf.clauses.size(); ++i) {
        if (clauseDeleted[i]) continue;
        int count = 0;
        for (const auto& node : cnf.clauses[i]) {
            int assignedValue = assignment[node.var - 1];
            if (assignedValue == -1) {
                count++;
                lastUnassignedNode[i] = node;
            }
            else if (assignedValue == (node.negated ? 1 : 0)) {
                clauseDeleted[i] = true;
                clauseChangeLog.push_back(i);  
                break;
            }
        }
        unassignedCount[i] = count;
        if (count == 1 && !clauseDeleted[i]) {
            int literal = lastUnassignedNode[i].var * (lastUnassignedNode[i].negated ? 1 : -1);
            if (!propagateLiteral(literal, cnf, assignment, clauseChangeLog, clauseDeleted, unassignedCount, lastUnassignedNode)) {
                return false; 
            }
        }
    }
    return true;
}


// 获取未满足的子句索引
vector<int> getUnsatisfiedClauses(const vector<bool>& clauseDeleted, const CNFFormula& cnf) {
    vector<int> unsatisfiedClauses;
    unsatisfiedClauses.reserve(count(clauseDeleted.begin(), clauseDeleted.end(), false));

    for (size_t i = 0; i < clauseDeleted.size(); ++i) {
        if (!clauseDeleted[i]) {
            unsatisfiedClauses.push_back(i);
        }
    }

    return unsatisfiedClauses;
}

int minSize;
// 获取最小子句的索引集合
vector<int> getSmallestClauses(const vector<int>& clauses, const CNFFormula& cnf, const vector<bool>& clauseDeleted, vector<int>& unassignedCount) {
    if (clauses.empty()) {
        return {};
    }
    minSize = cnf.clauses[clauses[0]].size();  
    vector<int> smallestClauses;  
    for (int clauseIndex : clauses) {
        if (clauseDeleted[clauseIndex] == true) {
            continue;
        }
        int clauseSize = unassignedCount[clauseIndex];
        if (clauseSize < minSize) {
            minSize = clauseSize;  
            smallestClauses.clear(); 
            smallestClauses.push_back(clauseIndex);  
        }
        else if (clauseSize == minSize) {
            smallestClauses.push_back(clauseIndex); 
        }
    }
    return smallestClauses;
}



// 计算两个子句集合的差异数量（对比字句的文字）
int countDiffClauses(const vector<int>& clause1, const vector<bool>& clauseDeleted, vector<int>& unassignedCount) {
    int diffCount = 0;
    for (int lit : clause1) {
        // 检查 lit 是否有效并满足条件
        if (!clauseDeleted[lit] && unassignedCount[lit] != minSize) {
            ++diffCount;
        }
    }
    return diffCount;
}


// 返回拥有最大启发值的变元
int getMaxVar(std::unordered_map<int, int>& H, const std::vector<int>& assignment) {
    int maxVar = -1;
    int maxHeuristic = INT_MIN;
    std::vector<int> candidates;  

    for (const auto& [var, heuristic] : H) {
        if (assignment[var - 1] == -1) {
            if (heuristic > maxHeuristic) {
                maxHeuristic = heuristic;
                maxVar = var;
                candidates.clear();  
                candidates.push_back(var); 
            }
            else if (heuristic == maxHeuristic) {
                candidates.push_back(var);  
            }
        }
    }

    if (!candidates.empty()) {
        static std::mt19937 rng(std::time(0)); 
        std::uniform_int_distribution<int> dist(0, candidates.size() - 1);
        return candidates[dist(rng)]; 
    }

    return maxVar; 
}
int up(const vector<int>& prop,const  CNFFormula& cnf,  vector<int>& assignment,
    vector<bool>& clauseDeleted, vector<int>& clauseChangeLog, vector<int>& unassignedCount,
    vector<Node>& lastUnassignedNode, vector<pair<int, int>>& trail) {
    vector<int> ass = assignment;
    vector<bool> Del = clauseDeleted;
    vector<int> ChangeLog = clauseChangeLog;
    vector<int> uc = unassignedCount;
    vector<Node> lu = lastUnassignedNode;
    unordered_map<int, int> H;
    bool sat = false;
    int i = 0;
    for (int index : prop) {
        i += 1;
        index = index + 1;
        try {
            const vector<int>& Clauses = cnf.getClausesWithLiteral(index);
            if (&Clauses == nullptr) {
                continue;
            }
        }
        catch (const std::exception& e) {
            continue;
        }
        vector<int> ass1 = assignment, ass2 = assignment;
        vector<bool> Del1 = clauseDeleted, Del2 = clauseDeleted;
        vector<int> ChangeLog1 = clauseChangeLog, ChangeLog2 = clauseChangeLog;
        vector<int> uc1 = unassignedCount, uc2 = unassignedCount;
        vector<Node> lu1 = lastUnassignedNode, lu2 = lastUnassignedNode;
        // 传递文字并更新子句状态
        bool result = propagateLiteral(index, cnf, ass1, ChangeLog1, Del1, uc1, lu1);

        auto F1 = getUnsatisfiedClauses(Del1, cnf); // 获取未满足的子句索引
        if (F1.size() == 0) {
            return index;
        }
        bool results = propagateLiteral(-index, cnf, ass2, ChangeLog2, Del2, uc2, lu2);
        if (!results&&!result) {
            continue;
        }
        auto F2 = getUnsatisfiedClauses(Del2, cnf);
        if (!result && results) {
            assignment = ass2;
            trail.push_back({ index - 1, 0 });
            unassignedCount = uc2;
            clauseDeleted = Del2;
            clauseChangeLog = ChangeLog2;
            lastUnassignedNode = lu2;
            continue;
        }
        else if (result && !results) {
            assignment = ass1;
            trail.push_back({ index - 1, 1 });
            unassignedCount = uc1;
            clauseDeleted = Del1;
            clauseChangeLog = ChangeLog1;
            lastUnassignedNode = lu1;
            continue;
        }
        if (F2.size() == 0) {
            return index;
        }
        if (F1.size() == cnf.clauses.size()&& F2.size() == cnf.clauses.size()) {
            continue;
        }
        
        // 根据索引获取最小子句
        auto Q1 = getSmallestClauses(F1, cnf, Del1,uc1);
        auto Q2 = getSmallestClauses(F2, cnf, Del2,uc2);
        // 计算子句差异数量
        int w1 = countDiffClauses(Q1, clauseDeleted,unassignedCount);
        int w2 = countDiffClauses(Q2, clauseDeleted,unassignedCount);
        sat = true;
        // 更新启发值
        H[index] = w1 * w2 * 1024 + w1 + w2;
        if (!sat) {
            if (i > 400) {
                break;
            }
        }
        else {
            if (i > 300) {
               
                break;
            }
        }
        
    }
    if (!sat) {
        return -1;
    }
    assignment = ass;
    unassignedCount = uc;
    clauseDeleted = Del;
    clauseChangeLog = ChangeLog;
    lastUnassignedNode = lu;
    return getMaxVar(H, assignment);  // 返回最佳变元
}
int prop(CNFFormula& cnf,  vector<int>& assignment, vector<bool>& clauseDeleted,
    vector<int>& clauseChangeLog, vector<int>& unassignedCount, vector<Node>& lastUnassignedNode, vector<pair<int, int>>& trail) {

    int T = 10;
    vector<int>  prop0;

    vector<int> a(2 * cnf.numVars, 0);
    int unassignedTwoCount = 0;
    for (int i = 0; i < unassignedCount.size(); ++i) {
        if (unassignedCount[i] == 2) {
            ++unassignedTwoCount;
            if (unassignedTwoCount >= 5) {
                break;  
            }
        }
    }
    if (unassignedTwoCount < 5) {
        for (int x = 0; x < cnf.numVars; ++x) {
            if (assignment[x] == -1) {
                prop0.push_back(x);
            }
        }
        return up(prop0, cnf, assignment, clauseDeleted, clauseChangeLog, unassignedCount, lastUnassignedNode, trail);
    }
    vector<int> prop41, prop31,prop21;
    // 统计每个未赋值变元（x和-x）在未满足的二元子句中出现的次数
    for (int i = 0; i < cnf.clauses.size(); ++i) {
        if (!clauseDeleted[i] && unassignedCount[i] == 2) {
            for (const auto& node : cnf.clauses[i]) {
                int var = node.var - 1;
                if (assignment[abs(var)] == -1) {
                    if (node.negated) {
                        a[var]++;
                    }
                    else {
                        a[cnf.numVars + abs(var)]++;
                    }
                }
            }
        }
    }

    for (int x = 0; x < cnf.numVars; ++x) {
        if (assignment[x] == -1) {
            if (a[x] >= 1 && a[cnf.numVars + x] >= 1) {
                if (a[x] >= 4) {
                    prop41.push_back(x);
                }

                if (a[x] >= 3) {

                    prop31.push_back(x);
                }
                if (a[x] >= 2) {
                    prop21.push_back(x);
                }
            }
            prop0.push_back(x);

        }
    }
    prop41.insert(prop41.end(), prop31.begin(), prop31.end());
    prop41.insert(prop41.end(), prop21.begin(), prop21.end());
    prop41.insert(prop41.end(), prop0.begin(), prop0.end());
    // 返回UP启发的结果
    if (prop41.size() >= T) {
        return up(prop41, cnf, assignment, clauseDeleted, clauseChangeLog, unassignedCount, lastUnassignedNode, trail);
    }
    else if (prop31.size() >= T) {
        return up(prop31, cnf, assignment, clauseDeleted, clauseChangeLog, unassignedCount, lastUnassignedNode, trail);
    }
    else {
        return up(prop0, cnf, assignment, clauseDeleted, clauseChangeLog, unassignedCount, lastUnassignedNode, trail);
    }
}



bool dpllIterative(CNFFormula& cnf, vector<int>& assignment) {
    stack<vector<pair<int, int>>> stateStack;
    vector<pair<int, int>> trail;
    vector<bool> clauseDeleted(cnf.clauses.size(), false);
    stack<vector<int>> changeLogStack;
    vector<int> clauseChangeLog;
    vector<int> pureLiterals;
    changeLogStack.push(clauseChangeLog);
    stateStack.push(trail);
    pureLiteralElimination(cnf, assignment, clauseDeleted, pureLiterals);
    while (!stateStack.empty()) {
        trail = stateStack.top();
        stateStack.pop();
        fill(assignment.begin(), assignment.end(), -1);
        for (const int a : pureLiterals) {
            if (a < 0) {
                assignment[abs(a) - 1] = 0;
            }
            else {
                assignment[abs(a) - 1] = 1;
            }

        }
        for (size_t i = 0; i < trail.size(); ++i) {
            int index = trail[i].first;
            int value = trail[i].second;
            assignment[index] = value;
        }

        if (!changeLogStack.empty()) {
            auto changes = changeLogStack.top();
            changeLogStack.pop();
            for (int clauseIndex : changes) {
                clauseDeleted[clauseIndex] = false;
            }
        }
        vector<int> unassignedCount(cnf.clauses.size(), 0);
        vector<Node> lastUnassignedNode(cnf.clauses.size());
        bool result = unitPropagation(cnf, assignment, clauseChangeLog, clauseDeleted,unassignedCount, lastUnassignedNode);
        bool fin_result = isSatisfied(cnf, assignment);
        if (fin_result) {
            return true;
        }
        changeLogStack.push(clauseChangeLog);
        clauseChangeLog.clear();
        if (!stateStack.empty() && !result) {
            continue;
        }

        int var = prop(cnf, assignment,clauseDeleted,clauseChangeLog,unassignedCount,lastUnassignedNode, trail);
        if (var == -1) {
            continue;
        }
        //cout << "当前选择的变元" << var << endl;
        
        trail.push_back({ var - 1, 1 });
        stateStack.push(trail);
        trail.back().second = 0;
        stateStack.push(trail);
    }
    return false;
}


int main() {
    CNFFormula cnf = readCNF("D:/Desktop/SAT测试备选算例/Beijing/e0ddr2-10-by-5-1.cnf");
   // CNFFormula cnf = readCNF("D:/Desktop/SAT测试备选算例/基准算例/功能测试/sat-20.cnf");
    auto start = high_resolution_clock::now();
    vector<int> assignment(cnf.numVars, -1);
    bool result = dpllIterative(cnf, assignment);
    auto stop = high_resolution_clock::now();
    auto duration = duration_cast<milliseconds>(stop - start);

    if (result) {
        cout << "问题有解" << endl;
        for (int i = 0; i < cnf.numVars; ++i) {
            //可真可假
            if (assignment[i]==-1){
                assignment[i] = 1;
            }
            cout << "变元 " << i + 1 << " 的赋值为: " << (assignment[i]) << endl;
        }
    }
    else {
        cout << "问题无解" << endl;
    }
    cout << "算法运行时间: " << duration.count() / 1000.0 << " 秒" << endl;
    return 0;
}
//1
//int main() {
//    CNFFormula cnf = readCNF("D:/Desktop/SAT测试备选算例/Beijing/4blocksb.cnf");
//    auto start = high_resolution_clock::now();
//    vector<int> assignment(cnf.numVars, -1);
//    bool result = dpllIterative(cnf, assignment);
//    auto stop = high_resolution_clock::now();
//    auto duration = duration_cast<milliseconds>(stop - start);
//
//    // 创建输出文件流
//    ofstream outputFile("output.txt");
//    if (!outputFile.is_open()) {
//        cerr << "无法打开文件输出文件." << endl;
//        return 1; // 返回错误码
//    }
//
//    if (result) {
//        outputFile << "问题有解" << endl; // 写入文件
//        for (int i = 0; i < cnf.numVars; ++i) {
//            // 可真可假
//            if (assignment[i] == -1) {
//                assignment[i] = 1;
//            }
//            outputFile << "变元 " << i + 1 << " 的赋值为: " << (assignment[i]) << endl; // 写入文件
//        }
//    }
//    else {
//        outputFile << "问题无解" << endl; // 写入文件
//    }
//    outputFile << "算法运行时间: " << duration.count() / 1000.0 << " 秒" << endl; // 写入文件
//
//    // 关闭文件
//    outputFile.close();
//
//    return 0;
//}